the_es:ES, l:IdLnk, e:E. sends(l;e)  (Msg on l) List 

latex

Definitions

t  T, Id, P  Q, x:A. B(x), sender(e), s = t, rcv?(e), b, Type, Prop, A & B, x:AB(x), P  Q, pred!(e;e'), pred(e), first(e), A, a<b, x:AB(x), , {x:A| B(x) }, x:A. B(x), SWellFounded(R(x;y)), IdLnk, <a,b>, True, T, Msg(M), haslink(l;m), type List, P & Q, tag(k), lnk(k), act(k), islocal(k), Msg_sub(l;M), rcv(l,tg), Void, False, Knd, x,y. t(x;y), x. t(x), EOrderAxioms(E; pred?; info), sends(dE;dL;pred?;info;val;p;e;l), es-M(es), es-oaxioms(es), es_val(es), es_info(es), es-pred?(es), es-eq(es), Msg, sends(l;e), (Msg on l), E, ES, f(a), kindcase(k; a.f(a); l,t.g(l;t) ), x.A(x), IdLnkDeq

Lemmas

event system wf, better-sends wf, idlnk-deq wf, kindcase wf, Knd wf, haslink wf, Msg wf, squash wf, true wf, IdLnk wf, nat wf, not wf, first wf, pred wf, assert wf, rcv? wf, sender wf, Id wf